the_w:World, e, e':E. FairFifo  e <c e'  time(e)<time(e') 

latex

Definitions

World, t  T, x:A. B(x), E, FairFifo, P  Q, e <c e', time(e), a<b, R^+, sender(e), s = t, kind(e), isrcv(k), b, A & B, e <loc e', P  Q, x.A(x), rel_exp(T;R;n), x f y, , x:AB(x), left+right, Type, Prop, P & Q, , {x:A| B(x) }, x:AB(x), AB, i  j < k, {T}, lnk(k), match(l;t;t'), #$n, {i..j}, x:A. B(x), False, A, mu(f), , Dec(P), i=j, SQType(T), s ~ t, Void, f(a), b, , P  Q, Unit, if b t else f fi, n-m, -n, n+m

Lemmas

eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, nat plus wf, nat plus properties, rel exp wf, decidable int equal, mu wf, decidable le, w-match-exists, mu-property, le wf, w-match wf, lnk wf, w-time wf, nat wf, w-locl wf, assert wf, isrcv wf, w-ekind wf, w-sender wf, w-causl wf, fair-fifo wf, w-E wf, world wf